<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>MinProofStepStmt</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="MinProofStepStmt";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/gmff/MinHypothesisStep.html" title="class in mmj.gmff"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/gmff/MinProofWorksheet.html" title="class in mmj.gmff"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/gmff/MinProofStepStmt.html" target="_top">Frames</a></li>
<li><a href="MinProofStepStmt.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.gmff</div>
<h2 title="Class MinProofStepStmt" class="title">Class MinProofStepStmt</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li><a href="../../mmj/gmff/MinProofWorkStmt.html" title="class in mmj.gmff">mmj.gmff.MinProofWorkStmt</a></li>
<li>
<ul class="inheritance">
<li>mmj.gmff.MinProofStepStmt</li>
</ul>
</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<dl>
<dt>Direct Known Subclasses:</dt>
<dd><a href="../../mmj/gmff/MinDerivationStep.html" title="class in mmj.gmff">MinDerivationStep</a>, <a href="../../mmj/gmff/MinHypothesisStep.html" title="class in mmj.gmff">MinHypothesisStep</a></dd>
</dl>
<hr>
<br>
<pre>public class <span class="strong">MinProofStepStmt</span>
extends <a href="../../mmj/gmff/MinProofWorkStmt.html" title="class in mmj.gmff">MinProofWorkStmt</a></pre>
<div class="block">General object representing a proof step statement in a MinProofWorksheet.
 <p>
 The term "proof step" in Proof Worksheet terminology is any Proof Worksheet
 statement that contains a formula -- these are <code>MinHypothesisStep</code> and
 <code>MinDerivationStep</code>, the latter includes the final step, the "qed"
 step.</div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/gmff/MinProofStepStmt.html#MinProofStepStmt(mmj.gmff.MinProofWorksheet, java.lang.String[][])">MinProofStepStmt</a></strong>(<a href="../../mmj/gmff/MinProofWorksheet.html" title="class in mmj.gmff">MinProofWorksheet</a>&nbsp;w,
                java.lang.String[][]&nbsp;slc)</code>
<div class="block">Standard MinProofStepStmt constructor.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/MinProofStepStmt.html#buildModelAExport(mmj.gmff.GMFFExporter, java.lang.StringBuilder)">buildModelAExport</a></strong>(<a href="../../mmj/gmff/GMFFExporter.html" title="class in mmj.gmff">GMFFExporter</a>&nbsp;gmffExporter,
                 java.lang.StringBuilder&nbsp;exportBuffer)</code>
<div class="block">Formats export data for the proof step statement according to the
 <code>Model A</code> specifications and loads the data into a specified
 buffer.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_mmj.gmff.MinProofWorkStmt">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;mmj.gmff.<a href="../../mmj/gmff/MinProofWorkStmt.html" title="class in mmj.gmff">MinProofWorkStmt</a></h3>
<code><a href="../../mmj/gmff/MinProofWorkStmt.html#constructStmt(mmj.gmff.MinProofWorksheet, java.util.List)">constructStmt</a>, <a href="../../mmj/gmff/MinProofWorkStmt.html#getCleanedLineString(int)">getCleanedLineString</a>, <a href="../../mmj/gmff/MinProofWorkStmt.html#getCleanedLineString(int, int, int)">getCleanedLineString</a>, <a href="../../mmj/gmff/MinProofWorkStmt.html#isChunkWhitespace(java.lang.String)">isChunkWhitespace</a>, <a href="../../mmj/gmff/MinProofWorkStmt.html#typesetFormulaSymbols(mmj.gmff.GMFFExporter, java.lang.StringBuilder, java.lang.String[], int)">typesetFormulaSymbols</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="MinProofStepStmt(mmj.gmff.MinProofWorksheet, java.lang.String[][])">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>MinProofStepStmt</h4>
<pre>public&nbsp;MinProofStepStmt(<a href="../../mmj/gmff/MinProofWorksheet.html" title="class in mmj.gmff">MinProofWorksheet</a>&nbsp;w,
                java.lang.String[][]&nbsp;slc)</pre>
<div class="block">Standard MinProofStepStmt constructor.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>w</code> - the <code>MinProofworksheet</code> object which contains the proof
            step.</dd><dd><code>slc</code> - Array of proof step lines each comprised of an Array of
            <code>String</code>s called "chunks", which may be either Metamath
            whitespace or Metamath tokens. Hence the acronym "slc" refers
            to Statement Line Chunks.</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="buildModelAExport(mmj.gmff.GMFFExporter, java.lang.StringBuilder)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>buildModelAExport</h4>
<pre>public&nbsp;void&nbsp;buildModelAExport(<a href="../../mmj/gmff/GMFFExporter.html" title="class in mmj.gmff">GMFFExporter</a>&nbsp;gmffExporter,
                     java.lang.StringBuilder&nbsp;exportBuffer)
                       throws <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">Formats export data for the proof step statement according to the
 <code>Model A</code> specifications and loads the data into a specified
 buffer.
 <p>
 Model A model files for <code>MinProofStepStmt</code> objects are "mandatory",
 meaning that if any of the model files are not found, the export process
 is halted and an error message is generated.
 <p>
 Export of a proof step involves formatting two things: the part of each
 line prior to the first formula symbol on that line, and the typesetting
 and formatting of each formula symbol.
 <p>
 We go to a lot of trouble to format the pre-formula part of the line
 because it is vital to preserve the indentation before the formula
 symbols -- even though the process of generating typeset formulas will
 necessarily alter the indentations of the formula's symbols.
 <p>
 Note the quirky handling of <code>modelAStep1X</code> and <code>modelAStep3X</code>
 . If one of these model files is empty then no data is output at that
 location. This quirky feature will generally not be used but is provided
 for maximum flexibility in creating export format models.
 <p>
 Additional information may be found \GMFFDoc\GMFFModels.txt.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/gmff/MinProofWorkStmt.html#buildModelAExport(mmj.gmff.GMFFExporter, java.lang.StringBuilder)">buildModelAExport</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/gmff/MinProofWorkStmt.html" title="class in mmj.gmff">MinProofWorkStmt</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>gmffExporter</code> - The <code>GMFFExporter</code> requesting the export data
            build.</dd><dd><code>exportBuffer</code> - The <code>StringBuilder</code> to which exported data is
            to be output.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - if errors are encountered during the export
             process.</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/gmff/MinHypothesisStep.html" title="class in mmj.gmff"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/gmff/MinProofWorksheet.html" title="class in mmj.gmff"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/gmff/MinProofStepStmt.html" target="_top">Frames</a></li>
<li><a href="MinProofStepStmt.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
